On the existence and decidability of unique decompositions of processes in the applied π-calculus
Identifieur interne : 000693 ( Main/Exploration ); précédent : 000692; suivant : 000694On the existence and decidability of unique decompositions of processes in the applied π-calculus
Auteurs : Jannik Dreier [France] ; Cristian Ene [France] ; Pascal Lafourcade [France] ; Yassine Lakhnech [France]Source :
English descriptors
- mix :
Abstract
Unique decomposition has been a subject of interest in process algebra for a long time (for example in BPP [1] or CCS [2, 3]), as it provides a normal form and useful cancellation properties. We provide two parallel decomposition results for subsets of the applied π-calculus: we show that every closed normed (i.e. with a finite shortest complete trace) process P can be decomposed uniquely into prime factors P i with respect to strong labeled bisimilarity, i.e. such that P ∼ l P_1 | ... | P_n. Moreover, we prove that closed finite processes can be decomposed uniquely with respect to weak labeled bisimilarity. We also investigate whether efficient algorithms that compute the unique decompositions exist. The simpler problem of deciding whether a process is in its unique decomposition form is undecidable in general in both cases, due to potentially undecidable equational theories. Moreover, we show that the unique decomposition remains undecidable even given an equational theory with a decidable word problem.
Url:
DOI: 10.1016/j.tcs.2015.11.033
Affiliations:
- France
- Auvergne-Rhône-Alpes, Franche-Comté, Grand Est, Lorraine (région), Rhône-Alpes
- Belfort, Besançon, Grenoble, Metz, Nancy
- Université Joseph Fourier, Université de Bourgogne Franche-Comté, Université de Franche-Comté, Université de Grenoble, Université de Lorraine, Université de technologie de Belfort-Montbéliard
Links toward previous steps (curation, corpus...)
- to stream Hal, to step Corpus: 003832
- to stream Hal, to step Curation: 003832
- to stream Hal, to step Checkpoint: 000685
- to stream Main, to step Merge: 000690
- to stream Main, to step Curation: 000693
Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en">On the existence and decidability of unique decompositions of processes in the applied π-calculus</title><author><name sortKey="Dreier, Jannik" sort="Dreier, Jannik" uniqKey="Dreier J" first="Jannik" last="Dreier">Jannik Dreier</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-189789" status="VALID"><idno type="RNSR">200318302K</idno><orgName>Combination of approaches to the security of infinite states systems</orgName><orgName type="acronym">CASSIS</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.inria.fr/equipes/cassis</ref></desc><listRelation><relation active="#struct-423084" type="direct"></relation><relation active="#struct-206040" type="indirect"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-413289" type="indirect"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation><relation active="#struct-129671" type="direct"></relation><relation active="#struct-866" type="direct"></relation><relation active="#struct-242365" type="indirect"></relation><relation active="#struct-300261" type="indirect"></relation><relation active="#struct-300360" type="indirect"></relation><relation name="UMR6174" active="#struct-441569" type="indirect"></relation></listRelation><tutelles><tutelle active="#struct-423084" type="direct"><org type="department" xml:id="struct-423084" status="VALID"><orgName>Department of Formal Methods </orgName><orgName type="acronym">LORIA - FM</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.loria.fr/la-recherche-en/departements/formal-methods</ref></desc><listRelation><relation active="#struct-206040" type="direct"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-413289" type="indirect"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation></listRelation></org></tutelle><tutelle active="#struct-206040" type="indirect"><org type="laboratory" xml:id="struct-206040" status="VALID"><idno type="IdRef">067077927</idno><idno type="RNSR">198912571S</idno><idno type="IdUnivLorraine">[UL]RSI--</idno><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName><orgName type="acronym">LORIA</orgName><date type="start">2012-01-01</date><desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.loria.fr</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-413289" type="direct"></relation><relation name="UMR7503" active="#struct-441569" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-413289" type="indirect"><org type="institution" xml:id="struct-413289" status="VALID"><idno type="IdRef">157040569</idno><idno type="IdUnivLorraine">[UL]100--</idno><orgName>Université de Lorraine</orgName><orgName type="acronym">UL</orgName><date type="start">2012-01-01</date><desc><address><addrLine>34 cours Léopold - CS 25233 - 54052 Nancy cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.univ-lorraine.fr/</ref></desc></org></tutelle><tutelle name="UMR7503" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle><tutelle active="#struct-129671" type="direct"><org type="laboratory" xml:id="struct-129671" status="VALID"><idno type="RNSR">198618246Y</idno><orgName>INRIA Nancy - Grand Est</orgName><desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/nancy</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-866" type="direct"><org type="laboratory" xml:id="struct-866" status="VALID"><idno type="IdRef">152639071</idno><idno type="RNSR">200412232H</idno><orgName>Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies</orgName><orgName type="acronym">FEMTO-ST</orgName><desc><address><addrLine>32 avenue de l'Observatoire 25044 BESANCON CEDEX</addrLine><country key="FR"></country></address><ref type="url">http://www.femto-st.fr</ref></desc><listRelation><relation active="#struct-242365" type="direct"></relation><relation active="#struct-300261" type="direct"></relation><relation active="#struct-300360" type="direct"></relation><relation name="UMR6174" active="#struct-441569" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-242365" type="indirect"><org type="institution" xml:id="struct-242365" status="VALID"><idno type="IdRef">026403188</idno><idno type="ISNI">0000 0001 2188 3779 </idno><orgName>Université de Franche-Comté</orgName><orgName type="acronym">UFC</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.univ-fcomte.fr</ref></desc></org></tutelle><tutelle active="#struct-300261" type="indirect"><org type="institution" xml:id="struct-300261" status="VALID"><orgName>Université de Technologie de Belfort-Montbeliard</orgName><orgName type="acronym">UTBM</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300360" type="indirect"><org type="institution" xml:id="struct-300360" status="VALID"><orgName>Ecole Nationale Supérieure de Mécanique et des Microtechniques</orgName><orgName type="acronym">ENSMM</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle name="UMR6174" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle></tutelles></hal:affiliation><country>France</country><placeName><settlement type="city">Nancy</settlement><settlement type="city">Metz</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Université de Lorraine</orgName><placeName><settlement type="city" wicri:auto="siege">Besançon</settlement><region type="region" nuts="2">Franche-Comté</region></placeName><orgName type="university">Université de Franche-Comté</orgName><orgName type="institution" wicri:auto="newGroup">Université de Bourgogne Franche-Comté</orgName><placeName><settlement type="city" wicri:auto="siege">Belfort</settlement><region type="region" nuts="2">Franche-Comté</region></placeName><orgName type="university">Université de technologie de Belfort-Montbéliard</orgName></affiliation></author><author><name sortKey="Ene, Cristian" sort="Ene, Cristian" uniqKey="Ene C" first="Cristian" last="Ene">Cristian Ene</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-194" status="VALID"><orgName>VERIMAG</orgName><orgName type="acronym">VERIMAG - IMAG</orgName><desc><address><addrLine>Centre Équation - 2, avenue de Vignate - 38610 GIÈRES</addrLine><country key="FR"></country></address><ref type="url">http://www-verimag.imag.fr</ref></desc><listRelation><relation active="#struct-51016" type="direct"></relation><relation active="#struct-300275" type="direct"></relation><relation name="UMR5104" active="#struct-441569" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-51016" type="direct"><org type="institution" xml:id="struct-51016" status="OLD"><orgName>Université Joseph Fourier</orgName><orgName type="acronym">UJF</orgName><date type="end">2015-12-31</date><desc><address><addrLine>BP 53 - 38041 Grenoble Cedex 9</addrLine><country key="FR"></country></address><ref type="url">http://www.ujf-grenoble.fr/</ref></desc></org></tutelle><tutelle active="#struct-300275" type="direct"><org type="institution" xml:id="struct-300275" status="VALID"><orgName>Institut National Polytechnique de Grenoble (INPG)</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle name="UMR5104" active="#struct-441569" type="direct"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle></tutelles></hal:affiliation><country>France</country><placeName><settlement type="city">Grenoble</settlement><region type="region" nuts="2">Auvergne-Rhône-Alpes</region><region type="old region" nuts="2">Rhône-Alpes</region></placeName><orgName type="university">Université Joseph Fourier</orgName><orgName type="institution" wicri:auto="newGroup">Université de Grenoble</orgName></affiliation></author><author><name sortKey="Lafourcade, Pascal" sort="Lafourcade, Pascal" uniqKey="Lafourcade P" first="Pascal" last="Lafourcade">Pascal Lafourcade</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-857" status="OLD"><orgName>Laboratoire d'Informatique, de Modélisation et d'optimisation des Systèmes</orgName><orgName type="acronym">LIMOS</orgName><desc><address><addrLine>Bât ISIMA Campus des Cézeaux BP 10025 63173 AUBIERE cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.isima.fr/limos/</ref></desc><listRelation><relation active="#struct-157175" type="direct"></relation><relation active="#struct-205618" type="direct"></relation><relation active="#struct-300267" type="direct"></relation><relation name="UMR6158" active="#struct-441569" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-157175" type="direct"><org type="institution" xml:id="struct-157175" status="OLD"><orgName>Institut Français de Mécanique Avancée</orgName><orgName type="acronym">IFMA</orgName><desc><address><addrLine>Clermont Université, Institut Français de Mécanique Avancée (IFMA) / Laboratoire de Mécanique et Ingénieries (LaMI), BP 10448 - F-63000 Clermont Ferrand</addrLine><country key="FR"></country></address><ref type="url">http://www.ifma.fr/</ref></desc></org></tutelle><tutelle active="#struct-205618" type="direct"><org type="institution" xml:id="struct-205618" status="VALID"><orgName>Université Blaise Pascal - Clermont-Ferrand 2</orgName><orgName type="acronym">UBP</orgName><desc><address><addrLine>34, avenue Carnot - BP 185 - 63006 Clermont-Ferrand cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.univ-bpclermont.fr/</ref></desc></org></tutelle><tutelle active="#struct-300267" type="direct"><org type="institution" xml:id="struct-300267" status="VALID"><orgName>Université d'Auvergne - Clermont-Ferrand I</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle name="UMR6158" active="#struct-441569" type="direct"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle></tutelles></hal:affiliation><country>France</country></affiliation></author><author><name sortKey="Lakhnech, Yassine" sort="Lakhnech, Yassine" uniqKey="Lakhnech Y" first="Yassine" last="Lakhnech">Yassine Lakhnech</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-194" status="VALID"><orgName>VERIMAG</orgName><orgName type="acronym">VERIMAG - IMAG</orgName><desc><address><addrLine>Centre Équation - 2, avenue de Vignate - 38610 GIÈRES</addrLine><country key="FR"></country></address><ref type="url">http://www-verimag.imag.fr</ref></desc><listRelation><relation active="#struct-51016" type="direct"></relation><relation active="#struct-300275" type="direct"></relation><relation name="UMR5104" active="#struct-441569" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-51016" type="direct"><org type="institution" xml:id="struct-51016" status="OLD"><orgName>Université Joseph Fourier</orgName><orgName type="acronym">UJF</orgName><date type="end">2015-12-31</date><desc><address><addrLine>BP 53 - 38041 Grenoble Cedex 9</addrLine><country key="FR"></country></address><ref type="url">http://www.ujf-grenoble.fr/</ref></desc></org></tutelle><tutelle active="#struct-300275" type="direct"><org type="institution" xml:id="struct-300275" status="VALID"><orgName>Institut National Polytechnique de Grenoble (INPG)</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle name="UMR5104" active="#struct-441569" type="direct"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle></tutelles></hal:affiliation><country>France</country><placeName><settlement type="city">Grenoble</settlement><region type="region" nuts="2">Auvergne-Rhône-Alpes</region><region type="old region" nuts="2">Rhône-Alpes</region></placeName><orgName type="university">Université Joseph Fourier</orgName><orgName type="institution" wicri:auto="newGroup">Université de Grenoble</orgName></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">HAL</idno><idno type="RBID">Hal:hal-01238097</idno><idno type="halId">hal-01238097</idno><idno type="halUri">https://hal.archives-ouvertes.fr/hal-01238097</idno><idno type="url">https://hal.archives-ouvertes.fr/hal-01238097</idno><idno type="doi">10.1016/j.tcs.2015.11.033</idno><date when="2015">2015</date><idno type="wicri:Area/Hal/Corpus">003832</idno><idno type="wicri:Area/Hal/Curation">003832</idno><idno type="wicri:Area/Hal/Checkpoint">000685</idno><idno type="wicri:explorRef" wicri:stream="Hal" wicri:step="Checkpoint">000685</idno><idno type="wicri:Area/Main/Merge">000690</idno><idno type="wicri:Area/Main/Curation">000693</idno><idno type="wicri:Area/Main/Exploration">000693</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">On the existence and decidability of unique decompositions of processes in the applied π-calculus</title><author><name sortKey="Dreier, Jannik" sort="Dreier, Jannik" uniqKey="Dreier J" first="Jannik" last="Dreier">Jannik Dreier</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-189789" status="VALID"><idno type="RNSR">200318302K</idno><orgName>Combination of approaches to the security of infinite states systems</orgName><orgName type="acronym">CASSIS</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.inria.fr/equipes/cassis</ref></desc><listRelation><relation active="#struct-423084" type="direct"></relation><relation active="#struct-206040" type="indirect"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-413289" type="indirect"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation><relation active="#struct-129671" type="direct"></relation><relation active="#struct-866" type="direct"></relation><relation active="#struct-242365" type="indirect"></relation><relation active="#struct-300261" type="indirect"></relation><relation active="#struct-300360" type="indirect"></relation><relation name="UMR6174" active="#struct-441569" type="indirect"></relation></listRelation><tutelles><tutelle active="#struct-423084" type="direct"><org type="department" xml:id="struct-423084" status="VALID"><orgName>Department of Formal Methods </orgName><orgName type="acronym">LORIA - FM</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.loria.fr/la-recherche-en/departements/formal-methods</ref></desc><listRelation><relation active="#struct-206040" type="direct"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-413289" type="indirect"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation></listRelation></org></tutelle><tutelle active="#struct-206040" type="indirect"><org type="laboratory" xml:id="struct-206040" status="VALID"><idno type="IdRef">067077927</idno><idno type="RNSR">198912571S</idno><idno type="IdUnivLorraine">[UL]RSI--</idno><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName><orgName type="acronym">LORIA</orgName><date type="start">2012-01-01</date><desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.loria.fr</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-413289" type="direct"></relation><relation name="UMR7503" active="#struct-441569" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-413289" type="indirect"><org type="institution" xml:id="struct-413289" status="VALID"><idno type="IdRef">157040569</idno><idno type="IdUnivLorraine">[UL]100--</idno><orgName>Université de Lorraine</orgName><orgName type="acronym">UL</orgName><date type="start">2012-01-01</date><desc><address><addrLine>34 cours Léopold - CS 25233 - 54052 Nancy cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.univ-lorraine.fr/</ref></desc></org></tutelle><tutelle name="UMR7503" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle><tutelle active="#struct-129671" type="direct"><org type="laboratory" xml:id="struct-129671" status="VALID"><idno type="RNSR">198618246Y</idno><orgName>INRIA Nancy - Grand Est</orgName><desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/nancy</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-866" type="direct"><org type="laboratory" xml:id="struct-866" status="VALID"><idno type="IdRef">152639071</idno><idno type="RNSR">200412232H</idno><orgName>Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies</orgName><orgName type="acronym">FEMTO-ST</orgName><desc><address><addrLine>32 avenue de l'Observatoire 25044 BESANCON CEDEX</addrLine><country key="FR"></country></address><ref type="url">http://www.femto-st.fr</ref></desc><listRelation><relation active="#struct-242365" type="direct"></relation><relation active="#struct-300261" type="direct"></relation><relation active="#struct-300360" type="direct"></relation><relation name="UMR6174" active="#struct-441569" type="direct"></relation></listRelation></org></tutelle><tutelle active="#struct-242365" type="indirect"><org type="institution" xml:id="struct-242365" status="VALID"><idno type="IdRef">026403188</idno><idno type="ISNI">0000 0001 2188 3779 </idno><orgName>Université de Franche-Comté</orgName><orgName type="acronym">UFC</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.univ-fcomte.fr</ref></desc></org></tutelle><tutelle active="#struct-300261" type="indirect"><org type="institution" xml:id="struct-300261" status="VALID"><orgName>Université de Technologie de Belfort-Montbeliard</orgName><orgName type="acronym">UTBM</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300360" type="indirect"><org type="institution" xml:id="struct-300360" status="VALID"><orgName>Ecole Nationale Supérieure de Mécanique et des Microtechniques</orgName><orgName type="acronym">ENSMM</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle name="UMR6174" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle></tutelles></hal:affiliation><country>France</country><placeName><settlement type="city">Nancy</settlement><settlement type="city">Metz</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Université de Lorraine</orgName><placeName><settlement type="city" wicri:auto="siege">Besançon</settlement><region type="region" nuts="2">Franche-Comté</region></placeName><orgName type="university">Université de Franche-Comté</orgName><orgName type="institution" wicri:auto="newGroup">Université de Bourgogne Franche-Comté</orgName><placeName><settlement type="city" wicri:auto="siege">Belfort</settlement><region type="region" nuts="2">Franche-Comté</region></placeName><orgName type="university">Université de technologie de Belfort-Montbéliard</orgName></affiliation></author><author><name sortKey="Ene, Cristian" sort="Ene, Cristian" uniqKey="Ene C" first="Cristian" last="Ene">Cristian Ene</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-194" status="VALID"><orgName>VERIMAG</orgName><orgName type="acronym">VERIMAG - IMAG</orgName><desc><address><addrLine>Centre Équation - 2, avenue de Vignate - 38610 GIÈRES</addrLine><country key="FR"></country></address><ref type="url">http://www-verimag.imag.fr</ref></desc><listRelation><relation active="#struct-51016" type="direct"></relation><relation active="#struct-300275" type="direct"></relation><relation name="UMR5104" active="#struct-441569" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-51016" type="direct"><org type="institution" xml:id="struct-51016" status="OLD"><orgName>Université Joseph Fourier</orgName><orgName type="acronym">UJF</orgName><date type="end">2015-12-31</date><desc><address><addrLine>BP 53 - 38041 Grenoble Cedex 9</addrLine><country key="FR"></country></address><ref type="url">http://www.ujf-grenoble.fr/</ref></desc></org></tutelle><tutelle active="#struct-300275" type="direct"><org type="institution" xml:id="struct-300275" status="VALID"><orgName>Institut National Polytechnique de Grenoble (INPG)</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle name="UMR5104" active="#struct-441569" type="direct"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle></tutelles></hal:affiliation><country>France</country><placeName><settlement type="city">Grenoble</settlement><region type="region" nuts="2">Auvergne-Rhône-Alpes</region><region type="old region" nuts="2">Rhône-Alpes</region></placeName><orgName type="university">Université Joseph Fourier</orgName><orgName type="institution" wicri:auto="newGroup">Université de Grenoble</orgName></affiliation></author><author><name sortKey="Lafourcade, Pascal" sort="Lafourcade, Pascal" uniqKey="Lafourcade P" first="Pascal" last="Lafourcade">Pascal Lafourcade</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-857" status="OLD"><orgName>Laboratoire d'Informatique, de Modélisation et d'optimisation des Systèmes</orgName><orgName type="acronym">LIMOS</orgName><desc><address><addrLine>Bât ISIMA Campus des Cézeaux BP 10025 63173 AUBIERE cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.isima.fr/limos/</ref></desc><listRelation><relation active="#struct-157175" type="direct"></relation><relation active="#struct-205618" type="direct"></relation><relation active="#struct-300267" type="direct"></relation><relation name="UMR6158" active="#struct-441569" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-157175" type="direct"><org type="institution" xml:id="struct-157175" status="OLD"><orgName>Institut Français de Mécanique Avancée</orgName><orgName type="acronym">IFMA</orgName><desc><address><addrLine>Clermont Université, Institut Français de Mécanique Avancée (IFMA) / Laboratoire de Mécanique et Ingénieries (LaMI), BP 10448 - F-63000 Clermont Ferrand</addrLine><country key="FR"></country></address><ref type="url">http://www.ifma.fr/</ref></desc></org></tutelle><tutelle active="#struct-205618" type="direct"><org type="institution" xml:id="struct-205618" status="VALID"><orgName>Université Blaise Pascal - Clermont-Ferrand 2</orgName><orgName type="acronym">UBP</orgName><desc><address><addrLine>34, avenue Carnot - BP 185 - 63006 Clermont-Ferrand cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.univ-bpclermont.fr/</ref></desc></org></tutelle><tutelle active="#struct-300267" type="direct"><org type="institution" xml:id="struct-300267" status="VALID"><orgName>Université d'Auvergne - Clermont-Ferrand I</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle name="UMR6158" active="#struct-441569" type="direct"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle></tutelles></hal:affiliation><country>France</country></affiliation></author><author><name sortKey="Lakhnech, Yassine" sort="Lakhnech, Yassine" uniqKey="Lakhnech Y" first="Yassine" last="Lakhnech">Yassine Lakhnech</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-194" status="VALID"><orgName>VERIMAG</orgName><orgName type="acronym">VERIMAG - IMAG</orgName><desc><address><addrLine>Centre Équation - 2, avenue de Vignate - 38610 GIÈRES</addrLine><country key="FR"></country></address><ref type="url">http://www-verimag.imag.fr</ref></desc><listRelation><relation active="#struct-51016" type="direct"></relation><relation active="#struct-300275" type="direct"></relation><relation name="UMR5104" active="#struct-441569" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-51016" type="direct"><org type="institution" xml:id="struct-51016" status="OLD"><orgName>Université Joseph Fourier</orgName><orgName type="acronym">UJF</orgName><date type="end">2015-12-31</date><desc><address><addrLine>BP 53 - 38041 Grenoble Cedex 9</addrLine><country key="FR"></country></address><ref type="url">http://www.ujf-grenoble.fr/</ref></desc></org></tutelle><tutelle active="#struct-300275" type="direct"><org type="institution" xml:id="struct-300275" status="VALID"><orgName>Institut National Polytechnique de Grenoble (INPG)</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle><tutelle name="UMR5104" active="#struct-441569" type="direct"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle></tutelles></hal:affiliation><country>France</country><placeName><settlement type="city">Grenoble</settlement><region type="region" nuts="2">Auvergne-Rhône-Alpes</region><region type="old region" nuts="2">Rhône-Alpes</region></placeName><orgName type="university">Université Joseph Fourier</orgName><orgName type="institution" wicri:auto="newGroup">Université de Grenoble</orgName></affiliation></author></analytic><idno type="DOI">10.1016/j.tcs.2015.11.033</idno></biblStruct></sourceDesc></fileDesc><profileDesc><textClass><keywords scheme="mix" xml:lang="en"><term>Applied π-Calculus</term><term>Behavioural Equivalence</term><term>Cancellation</term><term>Decidability</term><term>Equational Theory</term><term>Normal Form</term><term>Process Calculus</term><term>Strong Bisimilarity</term><term>Unique Decomposition</term><term>Weak Bisimilarity</term><term>Word Problem</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Unique decomposition has been a subject of interest in process algebra for a long time (for example in BPP [1] or CCS [2, 3]), as it provides a normal form and useful cancellation properties. We provide two parallel decomposition results for subsets of the applied π-calculus: we show that every closed normed (i.e. with a finite shortest complete trace) process P can be decomposed uniquely into prime factors P i with respect to strong labeled bisimilarity, i.e. such that P ∼ l P_1 | ... | P_n. Moreover, we prove that closed finite processes can be decomposed uniquely with respect to weak labeled bisimilarity. We also investigate whether efficient algorithms that compute the unique decompositions exist. The simpler problem of deciding whether a process is in its unique decomposition form is undecidable in general in both cases, due to potentially undecidable equational theories. Moreover, we show that the unique decomposition remains undecidable even given an equational theory with a decidable word problem.</div></front></TEI><affiliations><list><country><li>France</li></country><region><li>Auvergne-Rhône-Alpes</li><li>Franche-Comté</li><li>Grand Est</li><li>Lorraine (région)</li><li>Rhône-Alpes</li></region><settlement><li>Belfort</li><li>Besançon</li><li>Grenoble</li><li>Metz</li><li>Nancy</li></settlement><orgName><li>Université Joseph Fourier</li><li>Université de Bourgogne Franche-Comté</li><li>Université de Franche-Comté</li><li>Université de Grenoble</li><li>Université de Lorraine</li><li>Université de technologie de Belfort-Montbéliard</li></orgName></list><tree><country name="France"><region name="Grand Est"><name sortKey="Dreier, Jannik" sort="Dreier, Jannik" uniqKey="Dreier J" first="Jannik" last="Dreier">Jannik Dreier</name></region><name sortKey="Ene, Cristian" sort="Ene, Cristian" uniqKey="Ene C" first="Cristian" last="Ene">Cristian Ene</name><name sortKey="Lafourcade, Pascal" sort="Lafourcade, Pascal" uniqKey="Lafourcade P" first="Pascal" last="Lafourcade">Pascal Lafourcade</name><name sortKey="Lakhnech, Yassine" sort="Lakhnech, Yassine" uniqKey="Lakhnech Y" first="Yassine" last="Lakhnech">Yassine Lakhnech</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000693 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 000693 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= Hal:hal-01238097
|texte= On the existence and decidability of unique decompositions of processes in the applied π-calculus
}}
| This area was generated with Dilib version V0.6.33. |  |